/*!
 * \file set_relation.cc
 *
 * \brief Implementations of the Set and Relation classes.
 *
 * \date Started: 6/8/2010
 * \date Last Modified: 7/6/2010
 * \authors Alan LaMielle
 * \authors Ian Craig
 * \authors Nicholas Jeanette
 */

#include <iegenlib/iegenlib.h>

#include <sstream>
#include <algorithm>
#include <assert.h>
using std::equal;
using std::stringstream;
#include <iostream>
using std::cout;
using std::endl;

#include <isl/flow.h>
#include <isl/constraint.h>
#include <isl/ctx.h>
#include <isl/set.h>
#include <isl/map.h>
#include <isl/printer.h>

namespace iegenlib{

/******************************** SRConstraint **********************************/
bool SRConstraint::any(SymType type,int& pos,int& coeff) const{
  return this->getExpVec().any(type,pos,coeff);
}

bool SRConstraint::any(SymType type,int pos,SymbolTable const*const sym_table) const{
  return this->getExpVec().any(type,pos,sym_table);
}
/********************************************************************************/

/******************************** SREquality **********************************/
void SREquality::apply(SRVisitor* visitor) const{
  visitor->SREqualityCase(this);
}

SREquality SREquality::replaceExistential(SymbolTable *sym_table,
                                          int exist_pos,
                                          ExpVec equal_exp) const{
  ExpVec constraint_exp=
    this->getExpVec().replaceExistential(sym_table,exist_pos,equal_exp);
  constraint_exp.normalizeEquality();
  return SREquality(constraint_exp);
}
/******************************************************************************/

/******************************* SRInequality *********************************/
void SRInequality::apply(SRVisitor* visitor) const{
  visitor->SRInequalityCase(this);
}

SRInequality SRInequality::replaceExistential(SymbolTable *sym_table,
                                              int exist_pos,
                                              ExpVec equal_exp) const{
  return SRInequality(this->getExpVec().replaceExistential(sym_table,exist_pos,
                                                           equal_exp));
}
/******************************************************************************/

/****************************** SRConjunction *********************************/
void SRConjunction::apply(SRVisitor* visitor) const{
  visitor->SRConjunctionCase(this);
}

void SRConjunction::applyTuples(SRVisitor* visitor) const{
  for(list<TupleType>::const_iterator it = tuplevars.begin();
      it != tuplevars.end(); ++it){
    it->apply(visitor);
  }
}

void SRConjunction::applyEqualities(SRVisitor* visitor) const{
  for(set<SREquality>::iterator it = equalities.begin(); it != equalities.end();
      ++it){
    it->apply(visitor);
  }
}

void SRConjunction::applyInequalities(SRVisitor* visitor) const{
  for(set<SRInequality>::iterator it = inequalities.begin();
      it != inequalities.end(); ++it){
    it->apply(visitor);
  }
}

const bool SRConjunction::operator<(const SRConjunction& op2) const{
  if(equalities.size() < op2.equalities.size()) return true;
  else if(equalities.size() > op2.equalities.size()) return false;
  else if(inequalities.size() < op2.inequalities.size()) return true;
  else if(inequalities.size() > op2.inequalities.size()) return false;
  if(equalities < op2.equalities) return true;
  if(inequalities < op2.inequalities) return true;
  return false;//they are equal
}

const bool SRConjunction::operator==(const SRConjunction& op2) const{
  if(this->tuplevars.size() != op2.tuplevars.size()){
    return false;
  }
  for(list<TupleType>::const_iterator
      tItr = this->tuplevars.begin(), oItr = op2.tuplevars.begin();
      tItr != this->tuplevars.end() && oItr != op2.tuplevars.end();
      ++tItr, ++oItr){
    if(tItr->isConst()){
      if(oItr->isVar()){
        return false;
      }else{
        if(tItr->getValue() != oItr->getValue()){
          return false;
        }
      }
    }
  }
  if(equalities.size() == op2.equalities.size() &&
  inequalities.size() == op2.inequalities.size() &&
  equalities == op2.equalities &&
  inequalities == op2.inequalities){
    return true;
  }else{
    return false;
  }
}

const bool SRConjunction::isEmpty() const {
  if(inequalities.empty() && equalities.empty()){
    return true;
  }else{
    return false;
  }
}

list<string> SRConjunction::tupleVarNames() const {
   list<string> names;
   for(list<TupleType>::const_iterator itr = this->tuplevarsBegin();
       itr != this->tuplevarsEnd(); ++itr){
      if(itr->isVar()){
         names.push_back(itr->getName());
      }
   }
   return names;
}

bool SRConjunction::check_for_matching_constants(SRConjunction op2,
    int other_start, int other_end) const{
  bool retBool = true;
  list<TupleType>::const_iterator tup2 = op2.tuplevarsBegin();
  //move this to the first tup for out arity in r2
  for(int i=0;i<other_start;++i){
    ++tup2;
  }

  //this loop runs from the start of the tuplevarsbegin for the 1st relation
  //and breaks out when the first relaion runs out of tuple vars (starting at
  //the start of its out arity)
  list<TupleType>::const_iterator tup1 = this->tuplevarsBegin();
  for(int i = other_start; i<= other_end; ++i){
    //checks that if the two tuples are const are they are the same?
    if(tup1->isConst() && tup2->isConst() && (tup1->getValue() != tup2->getValue())){
      retBool = false;
      break;
    }
    ++tup1;
    ++tup2;
  }
  return retBool;
}


list<TupleType> SRConjunction::make_new_tuple_list(list<TupleType> conj_tups_this,
    list<TupleType> conj_tups_other, int this_start, int this_end, int other_start,
    int other_end) const{
  list<TupleType> combTup;
  int tcount = 0;
  list<TupleType>::const_iterator it = conj_tups_other.begin();
  for(it; it!= conj_tups_other.end(); ++it){
    if(tcount >= other_start && tcount <= other_end){
      combTup.push_back(*it);
    }
    ++tcount;
  }

  tcount = 0;
  it =  conj_tups_this.begin();
  for(it; it != conj_tups_this.end();++it){
    if(tcount >= this_start && tcount <= this_end){
      combTup.push_back(*it);
    }
    ++tcount;
  }
  return combTup;
}

bool SRConjunction::getTopExistEqualExp(SymbolTable const*const sym_table,
                                        SREquality& equality_constraint,
                                        int& exist_pos,ExpVec& equal_exp) const{
  bool res=false;

  //Look for a top-level existential variable in this conjunctions equalities
  for(set<SREquality>::const_iterator curr_eq=this->equalities.begin();
      curr_eq!=this->equalities.end(); ++curr_eq){
    int coeff;
    if(curr_eq->any(EXISTENTIAL,exist_pos,coeff)){
      //The current constraint has a top-level existential variable
      //Is abs(coeff)==1?
      if(1==coeff || -1==coeff){
        equality_constraint=*curr_eq;
        ExpVec exist_exp=sym_table->constructExpVec();
        exist_exp.set_coeff(EXISTENTIAL,exist_pos,-1);
        equal_exp=((curr_eq->getExpVec()*coeff)+exist_exp)*-1;
        res=true;
        break;
      }
    }
  }

  return res;
}

bool SRConjunction::getInvFuncCandidate(SymbolTable *sym_table,
                           IEGenLibContext context,
                           SREquality& orig_eq,SREquality& new_eq) const{
  bool res=false;
  set<pair<string,string> > inverse_pairs=context.getInversePairs();

  //Look for an equality constraint that contains UFS expression with a
  // coefficient of 1 or -1, has a single argument, contains an existential
  // variable, and has an inverse pair in the given context.
  for(set<SREquality>::const_iterator curr_eq=this->equalities.begin();
      curr_eq!=this->equalities.end(); ++curr_eq){
    ExpVec eq_exp(curr_eq->getExpVec());

    //Look at each UFS coefficient
    for(int ufs_col=0; ufs_col<eq_exp.get_ufcalls_size(); ++ufs_col){
      int ufs_coeff=eq_exp.get_coeff(UFCALL,ufs_col);

      //Is the current UFS coefficient 1 or -1?
      if(1==ufs_coeff || -1==ufs_coeff){
        //Get the UFS STE and its parameters
        UFCall *ufs=sym_table->lookup_ufcall(ufs_col);
        list<ExpVec> ufs_params=ufs->getParams();

        //Does the UFS have a known inverse pair AND a single paramter?
        string inverse_name;
        if(1==ufs_params.size() &&
           context.hasInverse(ufs->getId(),inverse_name)){

          //Get the single parameter expression
          ExpVec param=*ufs_params.begin();
          int pos,coeff;

          //Does the single parameter contain at least one existential var?
          if(param.anyNesting(EXISTENTIAL,pos,coeff,sym_table)){
            //BINGO!  We have a candidate equality constraint

            //Construct an expression with just the UFS
            ExpVec ufs_exp=sym_table->constructExpVec();
            ufs_exp.set_coeff(UFCALL,ufs->getCol(),-1*ufs_coeff);

            //Subtract off the UFS term from the equality constraint expression
            ExpVec new_ufs_arg=eq_exp+ufs_exp;
            new_ufs_arg=new_ufs_arg*(-1*ufs_coeff);

            //Create a new UFCall
            UFCall *new_ufs=sym_table->lookup(inverse_name,list<ExpVec>(1,new_ufs_arg));

            //Create a new expression for the modified equality constraint
            ExpVec new_eq_exp=sym_table->constructExpVec();
            new_eq_exp.set_coeff(UFCALL,new_ufs->getCol(),1);

            //Create the final expression for the new equality
            new_eq_exp=(param*-1)+new_eq_exp;

            //Set the result variables
            orig_eq=*curr_eq;
            new_eq=SREquality(new_eq_exp);
            res=true;
            break;
          }
        }
      }
    }
    if(res){break;}
  }

  return res;
}

bool SRConjunction::getNestedInvFuncsCandidate(SymbolTable *sym_table,
                           IEGenLibContext context,
                           SREquality& orig_eq,SREquality& new_eq) const{
  bool res=false;

  //Look for an equality constraint that contains UFS expression with a
  // coefficient of 1 or -1, has a single argument, and has an inverse
  // pair in the given context.
  for(set<SREquality>::const_iterator curr_eq=this->equalities.begin();
      curr_eq!=this->equalities.end(); ++curr_eq){

    ExpVec eq_exp(curr_eq->getExpVec());

    //Look at each UFS coefficient
    for(int ufs_col=0; ufs_col<eq_exp.get_ufcalls_size(); ++ufs_col){
      int ufs_coeff=eq_exp.get_coeff(UFCALL,ufs_col);

      //Is the current UFS coefficient 1 or -1?
      if(1==ufs_coeff || -1==ufs_coeff){
        //Get the UFS STE and its parameters
        UFCall *ufs=sym_table->lookup_ufcall(ufs_col);
        list<ExpVec> ufs_params=ufs->getParams();

        //Does the UFS have a known inverse pair AND a single paramter?
        string inverse_name;
        if(1==ufs_params.size() &&
                context.hasInverse(ufs->getId(),inverse_name)){
          ExpVec param=*ufs_params.begin();
          //verify that the parameter of the UFS is an UFS of the 
          //form F(param), but not of the form F(param)+expression
          int pos, coeff;
          if(!(param.any(EXISTENTIAL,pos,coeff) ||
               param.any(SYMBOLIC,pos,coeff) ||
                param.any(CONST,pos,coeff) ||
                 param.any(TUPLE,pos,coeff)) ){
             int count=0;
             vector<int> coeffs=param.get_ufcalls_coeffs(); 
             for(int i=0; i<coeffs.size(); ++i){
               if(0!=coeffs[i]){
                 count=count+1;
                }// endif
              }// endfor
             if(count==1){
               //Look at each UFS coefficient in the parameter
               for(int ufs_col2=0; ufs_col2<param.get_ufcalls_size(); ++ufs_col2){
                 int ufs_coeff2=param.get_coeff(UFCALL,ufs_col2);
                 //Is the current UFS coefficient 1 or -1?
                 if(1==ufs_coeff2 || -1==ufs_coeff2){

                   //Get the inner UFS STE and its parameters
                   UFCall *ufs2=sym_table->lookup_ufcall(ufs_col2);
                   list<ExpVec> ufs_params2=ufs2->getParams();

                   //Does the inner UFS have a known inverse pair, and the inner UFS
                   //is the inverse pair of the outer UFS?
                   if(1==ufs_params2.size() && ufs2->getId()==inverse_name){
          
                      //get the parameter of the inner UFS
                      ExpVec param2=*ufs_params2.begin();

                      ExpVec ufs_exp2=sym_table->constructExpVec();
                      ufs_exp2.set_coeff(UFCALL,ufs2->getCol(),-1*ufs_coeff2);

                      ExpVec ufs_exp=sym_table->constructExpVec();
                      ufs_exp.set_coeff(UFCALL,ufs->getCol(),-1*ufs_coeff);

                      // simplify F(F_inve(expr1))=expr2 in the expression to become
                      // expr1=expr2
                      ExpVec new_ufs_arg=eq_exp+ufs_exp;
                      new_ufs_arg=new_ufs_arg*(-1*ufs_coeff);
                      new_ufs_arg=(param2*-1)+new_ufs_arg;
                    
                      //save the simplified expression in new_eq
                      new_eq=SREquality(new_ufs_arg);
                      orig_eq=*curr_eq;
                      res=true;
                      break;
                    } // endif
                  } // endif
                } // endfor
              }// endif
            }// endif
          }// endif
        }// endif
     }// endfor
      if(res==true){break;}
   }// endfor
  return res;
}

bool SRConjunction::any(SymType type,int pos,SymbolTable const*const sym_table) const{
  bool res=false;

  for(set<SREquality>::const_iterator equality=this->equalitiesBegin();
      equality!=this->equalitiesEnd(); ++equality){
    if(equality->any(type,pos,sym_table)){
      res=true;
      break;
    }
  }
  if(not res){
    for(set<SRInequality>::const_iterator inequality=this->inequalitiesBegin();
        inequality!=this->inequalitiesEnd(); ++inequality){
      if(inequality->any(type,pos,sym_table)){
        res=true;
        break;
      }
    }
  }

  return res;
}

SRConjunction SRConjunction::equalityReplacement(SymbolTable* sym_table)
                                                 const{
  SRConjunction conj(*this);
  int exist_pos;
  ExpVec equal_exp(sym_table->constructExpVec());
  SREquality equality_constraint(sym_table->constructExpVec());

  //Apply equality replacement until we can no longer do so
  while(conj.getTopExistEqualExp(sym_table,equality_constraint,exist_pos,equal_exp)){
    //Create a new simplified conjunction by replacing all instances of the
    //  existential with the expression it is equal to

    set<SREquality> new_equals;
    set<SRInequality> new_inequals;
    list<TupleType> conj_tups(conj.tuplevarsBegin(),
                              conj.tuplevarsEnd());

    //Replace all instances of the existential variable at pos exist_pos
    // with the expression that it is equal to equal_exp
    //Replacement in equality constraints
    for(set<SREquality>::const_iterator curr_eq=conj.equalitiesBegin();
        curr_eq!=conj.equalitiesEnd(); ++curr_eq){
      //Don't add the equality constraint we are replacing
      if(!(*curr_eq==equality_constraint)){
        //Add the equality constraint with the existential replaced
        new_equals.insert(curr_eq->replaceExistential(sym_table,exist_pos,
                                                      equal_exp));
      }
    }
    //Replacement in inequality constraints
    for(set<SRInequality>::const_iterator curr_ineq=conj.inequalitiesBegin();
        curr_ineq!=conj.inequalitiesEnd(); ++curr_ineq){
      //Add the inequality constraint with the existential replaced
      new_inequals.insert(curr_ineq->replaceExistential(sym_table,exist_pos,
                                                        equal_exp));
    }

    //Set the current conjunction to the new conjunction we just created
    conj=SRConjunction(new_equals,new_inequals,conj_tups);
  }

  return conj;
}

SRConjunction SRConjunction::inverseFunctionSimplify(SymbolTable* sym_table,
                                                     IEGenLibContext context)
                                                     const{
  SRConjunction conj(*this);
  SREquality orig_eq(sym_table->constructExpVec()),
             new_eq(sym_table->constructExpVec());

  //Find candidates for the inverse function simplification until there are none
  while(conj.getInvFuncCandidate(sym_table,context,orig_eq,new_eq)){
    //Create a new conjunction with the new equality constraint
    set<SREquality> new_equals;

    //Replace all instances of the existential variable at pos exist_pos
    // with the expression that it is equal to equal_exp
    //Replacement in equality constraints
    for(set<SREquality>::const_iterator curr_eq=conj.equalitiesBegin();
        curr_eq!=conj.equalitiesEnd(); ++curr_eq){
      //Replace the original equality constraint with the new one
      if(*curr_eq==orig_eq){
        new_equals.insert(new_eq);
      }
      else{
        new_equals.insert(*curr_eq);
      }
    }

    //Set the current conjunction to the new conjunction we just created
    conj=SRConjunction(new_equals,
             set<SRInequality>(conj.inequalitiesBegin(),conj.inequalitiesEnd()),
             list<TupleType>(conj.tuplevarsBegin(),conj.tuplevarsEnd()));

    //Replace the existential if one was exposed by the inverse simplification
    conj=conj.equalityReplacement(sym_table);
  }
  //Repleace func(func_inv(expr)) by expr
  conj=conj.NestingInvertedFunctionSimplify(sym_table, context);

  return conj;
}

SRConjunction SRConjunction::NestingInvertedFunctionSimplify(SymbolTable* sym_table,
                                                     IEGenLibContext context)
                                                     const{
  SRConjunction conj(*this);
  SREquality orig_eq(sym_table->constructExpVec()),
             new_eq(sym_table->constructExpVec());

  //Find candidates for the function(function_inv()) simplification
  // until there are none
  while(conj.getNestedInvFuncsCandidate(sym_table,context,orig_eq,new_eq)){
    //Create a new conjunction with the new equality constraint
    set<SREquality> new_equals;

    // replace the equality constraint f(f_inv(expr1))=expr2 by
    // expr1=expr2 
    for(set<SREquality>::const_iterator curr_eq=conj.equalitiesBegin();
        curr_eq!=conj.equalitiesEnd(); ++curr_eq){
      //Replace the original equality constraint with the new one
      if(*curr_eq==orig_eq){
        new_equals.insert(new_eq);
      }
      else{
        new_equals.insert(*curr_eq);
      }
    }

    //Set the current conjunction to the new conjunction we just created
    conj=SRConjunction(new_equals,
             set<SRInequality>(conj.inequalitiesBegin(),conj.inequalitiesEnd()),
             list<TupleType>(conj.tuplevarsBegin(),conj.tuplevarsEnd()));

  }
  return conj;
}

SRConjunction SRConjunction::getAffineConjunction() const{
  set<SREquality> affine_equalities;
  set<SRInequality> affine_inequalities;

  //Gather all affine equalities
  for(set<SREquality>::const_iterator eq=this->equalitiesBegin();
      eq!=this->equalitiesEnd(); ++eq){
    if(eq->isAffine()){
      affine_equalities.insert(*eq);
    }
  }

  //Gather all affine inequalities
  for(set<SRInequality>::const_iterator ineq=this->inequalitiesBegin();
      ineq!=this->inequalitiesEnd(); ++ineq){
    if(ineq->isAffine()){
      affine_inequalities.insert(*ineq);
    }
  }

  return SRConjunction(affine_equalities,affine_inequalities,this->tuplevars);
}

SRConjunction SRConjunction::getUFSConjunction() const{
  set<SREquality> ufs_equalities;
  set<SRInequality> ufs_inequalities;

  //Gather all ufs equalities
  for(set<SREquality>::const_iterator eq=this->equalitiesBegin();
      eq!=this->equalitiesEnd(); ++eq){
    if(!eq->isAffine()){
      ufs_equalities.insert(*eq);
    }
  }

  //Gather all ufs inequalities
  for(set<SRInequality>::const_iterator ineq=this->inequalitiesBegin();
      ineq!=this->inequalitiesEnd(); ++ineq){
    if(!ineq->isAffine()){
      ufs_inequalities.insert(*ineq);
    }
  }

  return SRConjunction(ufs_equalities,ufs_inequalities,this->tuplevars);
}
/******************************************************************************/

/**************************** SparseConstraints *******************************/

SparseConstraints::SparseConstraints(string pres_form, bool isSet,
    IEGenLibContext const context){
  try{
    if(isSet){
      PresSet* PS = iegenlib::pres_parser::parse_set(pres_form);
      Set* temp = NULL;
      list<Conjunction*>const cnjj =  PS->getConjuncts();
    for(list<Conjunction*>::const_iterator itr =cnjj.begin() ; itr != cnjj.end(); itr++){
      //Add all symbolics from the AST
      this->context = context;
      list<string> const * ast_syms = (PS->getSymbolics());
      for(list<string>::const_iterator sym_name=ast_syms->begin();
          sym_name!=ast_syms->end(); ++sym_name ){
          this->context.addSymbolic(Symbolic(*sym_name));
      }
      BuildSymTableVisitor stv(this->context.getSymbolicNames());
      (*itr)->apply(&stv);
      SymbolTable* sym_table = stv.getSymTable();
      inArity = stv.getInArity();
      outArity = 0;
      BuildSparseConstraints bsc(sym_table, stv.getEqualities(),
        stv.getTuples());
      (*itr)->apply(&bsc);
      set<SRConjunction> SRconj = set<SRConjunction>();
      SRconj.insert(bsc.getConjunction());
      Set* set=new Set(sym_table, SRconj, inArity, context);
      if(temp == NULL){
         temp = set;
         this->BSCVstring = bsc.toString();
      }else{
         Set* temp2 = new Set( temp->Union(*set) );
         delete temp;
         temp = temp2;
         delete set;
      }

    } // end for
      this->SymTable = new SymbolTable(*temp->SymTable);
      this->ConSet = temp->ConSet;
      this->isSet = isSet;
      delete temp;

      DotVisitor dot;
      PS->apply(&dot);
      astDot = dot.getString();
      delete PS;
    }else{
     PresRelation* PR = iegenlib::pres_parser::parse_relation(pres_form);

     Relation* temp = NULL;
     list<Conjunction*>const cnjj =  PR->getConjuncts();
    for(list<Conjunction*>::const_iterator itr =cnjj.begin() ; itr != cnjj.end(); itr++){
      //Add all symbolics from the AST
      this->context = context;
      list<string> const * ast_syms = (PR->getSymbolics());
      for(list<string>::const_iterator sym_name=ast_syms->begin();
          sym_name!=ast_syms->end(); ++sym_name){
          this->context.addSymbolic(Symbolic(*sym_name));
      }

      BuildSymTableVisitor stv(this->context.getSymbolicNames());
      (*itr)->apply(&stv);
      SymbolTable* sym_table = stv.getSymTable();
      inArity = stv.getInArity();
      outArity = stv.getOutArity();
      BuildSparseConstraints bsc(sym_table, stv.getEqualities(),
        stv.getTuples());
      (*itr)->apply(&bsc);

      set<SRConjunction> SRconj = set<SRConjunction>();
      SRconj.insert(bsc.getConjunction());
      Relation* rel=new Relation(sym_table, SRconj, inArity, outArity, context);
      if(temp == NULL){
         temp = rel;
         this->BSCVstring = bsc.toString();
      }else{
         Relation* temp2 = new Relation( temp->Union(*rel) );
         delete temp;
         temp = temp2;
         delete rel;
      }

    } // end for
      this->SymTable = new SymbolTable(*temp->SymTable);
      this->ConSet = temp->ConSet;
      this->isSet = isSet;
      delete temp;

      DotVisitor dot;
      PR->apply(&dot);
      astDot = dot.getString();
      delete PR;
    }
  }catch(string s){
    throw ParseException("Error parsing string '"+pres_form+"': "+s);
  }
  //Simplify the formula
  pair<SymbolTable*,set<SRConjunction> > res=this->simplify();
  delete this->SymTable;
  this->SymTable=res.first;
  this->ConSet=res.second;
}


SparseConstraints::SparseConstraints(const SparseConstraints& spc){

  this->SymTable = new SymbolTable(*spc.SymTable);

  this->isSet = spc.isSet;
  this->context = spc.context;
  this->ConSet = spc.ConSet;
  this->BSCVstring = spc.BSCVstring;
  this->inArity = spc.inArity;
  this->outArity = spc.outArity;
  this->astDot = spc.astDot;
}

SparseConstraints& SparseConstraints::operator=(const SparseConstraints& spc){
  //assert(this->SymTable == NULL);
  delete this->SymTable;
  this->SymTable = new SymbolTable(*spc.SymTable);

  this->isSet = spc.isSet;
  this->context = spc.context;
  this->ConSet = spc.ConSet;
  this->BSCVstring = spc.BSCVstring;
  this->inArity = spc.inArity;
  this->outArity = spc.outArity;
  this->astDot = spc.astDot;

  return *this;
}

void SparseConstraints::apply(SRVisitor* visitor) const{
  visitor->SparseConstraintsCase(this);
}

bool SparseConstraints::operator==(SparseConstraints const& other) const{
  set<string> symbolics,exists,tuple_vars;
  list<string> symbolics_this,symbolics_other;
  list<string> exists_this,exists_other;
  list<string> tuple_vars_this,tuple_vars_other;
  int num_ufcalls;
  set<string> symbols;
  map<string,string> old2newThis, old2newOther;
  SymbolTable *merged_symbol_table;


  //STEP 2: Gather info for new symbol table
  //Gather symbolics from both formulas
  symbolics_this=createUniqueNames(this->SymTable->symNamesBegin(),
    this->SymTable->symNamesEnd(),symbols,old2newThis);
  symbolics_other=createUniqueNames(other.SymTable->symNamesBegin(),
    other.SymTable->symNamesEnd(),symbols,old2newOther);
  symbolics=unionNamesLists(symbolics_this,symbolics_other);

  //Gather tuple variables from both formulas
  tuple_vars_this=this->getTupleVarNames();
  tuple_vars_this=createUniqueNames(tuple_vars_this.begin(),
    tuple_vars_this.end(),symbols,old2newThis);

  tuple_vars_other=other.getTupleVarNames();
  tuple_vars=set<string>(tuple_vars_this.begin(),tuple_vars_this.end());


  createMatchingNames(tuple_vars_this.begin(),tuple_vars_this.end(),
    tuple_vars_other.begin(),tuple_vars_other.end(),old2newOther);


  //Gather existential variables from both formulas
  //Note: This isn't needed as if there are any existentials then equality
  //      checks cannot be done
  exists=set<string>();

  //Calculate the upper bound on the number of function calls
  num_ufcalls = this->SymTable->getNumFuncs() + other.SymTable->getNumFuncs();

  //STEP 3: Create a symbol table based on the information gathered above
  merged_symbol_table=new SymbolTable(&tuple_vars,&symbolics,&exists,
    num_ufcalls);

  //STEP 4: Create new set of conjunctions
  set<SRConjunction> new_conjs_this;
  for(set<SRConjunction>::const_iterator itr = this->conSetBegin();
      itr!=this->conSetEnd(); ++itr) {

      SRConjunction conjunction=*itr;
      list<TupleType> conj_tups=renameTupleVars(conjunction.tuplevarsBegin(),
          conjunction.tuplevarsEnd(),old2newThis);
      MergeSymbolTableVisitor mstv(this->SymTable,merged_symbol_table,
          &old2newThis,conj_tups);
      conjunction.apply(&mstv);
      new_conjs_this.insert(mstv.getNewConjunction());
  }

  set<SRConjunction> new_conjs_other;
  for(set<SRConjunction>::const_iterator itr = other.conSetBegin();
      itr!=other.conSetEnd(); ++itr) {

      SRConjunction conjunction=*itr;
      list<TupleType> conj_tups=renameTupleVars(conjunction.tuplevarsBegin(),
          conjunction.tuplevarsEnd(),old2newOther);
      MergeSymbolTableVisitor mstv(other.SymTable,merged_symbol_table,
          &old2newOther,conj_tups);
      conjunction.apply(&mstv);
      new_conjs_other.insert(mstv.getNewConjunction());
  }

  delete merged_symbol_table;

  return (new_conjs_this==new_conjs_other);
}

pair<SymbolTable*,set<SRConjunction> > SparseConstraints::Union(
    SparseConstraints const& other) const{

  set<string> symbolics,exists,tuple_vars;
  list<string> symbolics_this,symbolics_other;
  list<string> exists_this,exists_other;
  list<string> tuple_vars_this,tuple_vars_other;
  int num_ufcalls;
  set<string> symbols;
  map<string,string> old2newThis, old2newOther;
  SymbolTable *merged_symbol_table;

  //STEP 2: Gather info for new symbol table
  //Gather symbolics from both formulas
  symbolics_this=createUniqueNames(this->SymTable->symNamesBegin(),
    this->SymTable->symNamesEnd(),symbols,old2newThis);
  symbolics_other=createUniqueNames(other.SymTable->symNamesBegin(),
    other.SymTable->symNamesEnd(),symbols,old2newOther);
  symbolics=unionNamesLists(symbolics_this,symbolics_other);

  //Gather tuple variables from both formulas
  tuple_vars_this=this->getTupleVarNames();
  tuple_vars_this=createUniqueNames(tuple_vars_this.begin(),
    tuple_vars_this.end(),symbols,old2newThis);

  tuple_vars=set<string>(tuple_vars_this.begin(),tuple_vars_this.end());

  tuple_vars_other=other.getTupleVarNames();

  createMatchingNames(tuple_vars_this.begin(),tuple_vars_this.end(),
    tuple_vars_other.begin(),tuple_vars_other.end(),old2newOther);

  //Gather existential variables from both formulas
  exists_this=createUniqueNames(this->SymTable->existNamesBegin(),
    this->SymTable->existNamesEnd(),symbols,old2newThis);
  exists_other=createUniqueNames(other.SymTable->existNamesBegin(),
    other.SymTable->existNamesEnd(),symbols,old2newOther);
  exists=unionNamesLists(exists_this,exists_other);

  //Calculate the upper bound on the number of function calls
  num_ufcalls = this->SymTable->getNumFuncs() + other.SymTable->getNumFuncs();

  //STEP 3: Create a symbol table based on the information gathered above
  merged_symbol_table=new SymbolTable(&tuple_vars,&symbolics,&exists,
    num_ufcalls);

  //STEP 4: Create new set of conjunctions
  set<SRConjunction> new_conjs;
  for(set<SRConjunction>::const_iterator itr = this->conSetBegin();
      itr!=this->conSetEnd(); ++itr) {

      SRConjunction conjunction=*itr;
      list<TupleType> conj_tups=renameTupleVars(conjunction.tuplevarsBegin(),
          conjunction.tuplevarsEnd(),old2newThis);
      MergeSymbolTableVisitor mstv(this->SymTable,merged_symbol_table,
          &old2newThis,conj_tups);
      conjunction.apply(&mstv);
      new_conjs.insert(mstv.getNewConjunction());
  }


  for(set<SRConjunction>::const_iterator itr = other.conSetBegin();
      itr!=other.conSetEnd(); ++itr) {

      SRConjunction conjunction=*itr;
      list<TupleType> conj_tups=renameTupleVars(conjunction.tuplevarsBegin(),
          conjunction.tuplevarsEnd(),old2newOther);
      MergeSymbolTableVisitor mstv(other.SymTable,merged_symbol_table,
          &old2newOther,conj_tups);
      conjunction.apply(&mstv);
      new_conjs.insert(mstv.getNewConjunction());
  }

  return make_pair(merged_symbol_table,new_conjs);
}

void SparseConstraints::checkArity(SparseConstraints const& other) const{
  if(this->inArity != other.inArity){
    throw UnionException("The inArity does not match what it should be.");
  }
  //Only check the outArity if we are a relation
  if(!this->isSet){
    if(this->outArity != other.outArity){
      throw UnionException("The outArity does not match what it should be.");
    }
  }
}

void SparseConstraints::checkConstVarMatchforUnion(SparseConstraints const& other) const{
  //make sure the insides have comparable items ie var var num num...
  for(set<SRConjunction>::const_iterator it2 = other.conSetBegin();
      it2!=other.conSetEnd();++it2){
    for(set<SRConjunction>::const_iterator it1 = this->conSetBegin();
        it1!=this->conSetEnd();++it1){
      //grab the list of tuples for the first, iterate to the start of out arity
      list<TupleType>::const_iterator tup1 = it1->tuplevarsBegin();

      //this loop runs from the start of tuplevarsbegin for the 1st set/relation
      //and checks that the elements from the start of tuplevarsbegin for the 2nd
      //set/relation also match up, as in vars with vars and consts with consts
      for(list<TupleType>::const_iterator tup2 = it2->tuplevarsBegin();
          tup2!=it2->tuplevarsEnd();++tup2){
        //checks that the two tuples are the same (var/const)
        if((tup1->isConst()!=tup2->isConst())){
          throw UnionException("A constant and non-constant are being mapping to "
            "each other");
        }
        ++tup1;
      }
    }
  }
}

list<string> SparseConstraints::getInputTupleVarNames() const{
  set<SRConjunction>::const_iterator tConj = this->conSetBegin();
  list<string> retlist;
  int count = 0;
  for(list<TupleType>::const_iterator itr = tConj->tuplevarsBegin();
       itr != tConj->tuplevarsEnd(); ++itr){
    if(count >= this->inArity){
      break;
    }
    if(itr->isVar()){
      retlist.push_back(itr->getName());
    }
    ++count;
  }
  return retlist;
}

list<string> SparseConstraints::getOutputTupleVarNames() const{
  set<SRConjunction>::const_iterator tConj = this->conSetBegin();
  list<string> retlist;
  int count = 0;
  for(list<TupleType>::const_iterator itr = tConj->tuplevarsBegin();
       itr != tConj->tuplevarsEnd(); ++itr){
    if(count >= this->inArity){
      if(itr->isVar()){
        retlist.push_back(itr->getName());
      }
    }
    ++count;
  }
  return retlist;
}

list<TupleType> SparseConstraints::getInputTupleVarTypes() const{
  set<SRConjunction>::const_iterator tConj = this->conSetBegin();
  list<TupleType> retlist;
  int count = 0;
  for(list<TupleType>::const_iterator itr = tConj->tuplevarsBegin();
       itr != tConj->tuplevarsEnd(); ++itr){
    if(count >= this->inArity){
      break;
    }
    retlist.push_back(*itr);
    ++count;
  }
  return retlist;
}

list<TupleType> SparseConstraints::getOutputTupleVarTypes() const{
  set<SRConjunction>::const_iterator tConj = this->conSetBegin();
  list<TupleType> retlist;
  int count = 0;
  for(list<TupleType>::const_iterator itr = tConj->tuplevarsBegin();
       itr != tConj->tuplevarsEnd(); ++itr){
    if(count >= this->inArity){
      retlist.push_back(*itr);
    }
    ++count;
  }
  return retlist;
}

pair<SymbolTable*,set<SRConjunction> > SparseConstraints::simplify() const{
  set<SRConjunction> new_conjs;
  SymbolTable* new_symtable;

  //Only simplify if the context says we should
  if(!this->context.getSimplifyConjunctions()){
    new_conjs=set<SRConjunction>(this->ConSet);
    new_symtable=new SymbolTable(*(this->SymTable));
  }
  //Do the simplification
  else{
    //Construct a new symbol table
    new_symtable=new SymbolTable(*(this->SymTable));

    //For each conjunction, create a new simplified conjunction
    for(set<SRConjunction>::const_iterator conj_itr=this->conSetBegin();
        conj_itr!=this->conSetEnd(); ++conj_itr){
      //Get the current conjunction
      SRConjunction curr_conj=*conj_itr;

      //Apply equality replacement
      curr_conj=curr_conj.equalityReplacement(new_symtable);

      //Apply inverse function simplification if needed
      curr_conj=curr_conj.inverseFunctionSimplify(new_symtable,this->context);

      //Separate the affine and UFS constraints and simplify just the affine
      // constraints individually
      curr_conj=this->affineSimplify(curr_conj,new_symtable);

      //Add the simplified conjunction to the set of simplified conjunctions
      new_conjs.insert(curr_conj);
    }

    //Remove all unused existential variables from the symbol table
    map<string,string> orig2reduced;
    SymbolTable* reduced_symtable=this->reduceSymTable(new_symtable,new_conjs,
                                                       orig2reduced);

    //Convert the conjunctions to use the new reduced symbol table
    new_conjs=this->convertToReduced(new_symtable,reduced_symtable,orig2reduced,
                                     new_conjs);

    //Free the original symbol table now that we have created a reduced version
    delete new_symtable;
    new_symtable=reduced_symtable;
  }

  return make_pair(new_symtable,new_conjs);
}

SymbolTable* SparseConstraints::reduceSymTable(SymbolTable* orig_symtable,
                                               set<SRConjunction> conjs,
                                               map<string,string> &orig2reduced)
                                               const{
  set<string> symbolics,exists,tuple_vars;
  list<string> symbolics_list,tuple_vars_list;
  int num_ufcalls;
  set<string> symbols;
  SymbolTable *reduced_symtable;

  //Gather info for reduced symbol table
  //Gather symbolics
  symbolics=set<string>(orig_symtable->symNamesBegin(),
                        orig_symtable->symNamesEnd());

  //Gather tuple variables
  tuple_vars_list=conjs.begin()->tupleVarNames();
  tuple_vars_list=createUniqueNames(tuple_vars_list.begin(),
    tuple_vars_list.end(),symbols,orig2reduced);
  tuple_vars=set<string>(tuple_vars_list.begin(),tuple_vars_list.end());

  //Gather existential variables
  //Check that each existential has at least one non-zero coefficient before
  //adding it
  for(list<STE*>::const_iterator exist_ste=orig_symtable->existBegin();
      exist_ste!=orig_symtable->existEnd(); ++exist_ste){
    //Check each conjunction
    for(set<SRConjunction>::const_iterator conj=conjs.begin();
        conj!=conjs.end(); ++conj){
      if(conj->any(EXISTENTIAL,(*exist_ste)->getCol(),orig_symtable)){
        exists.insert((*exist_ste)->getId());
        break;
      }
    }
  }

  //Calculate the upper bound on the number of function calls
  num_ufcalls= orig_symtable->getNumFuncs();

  //Create a symbol table based on the information gathered above
  reduced_symtable=new SymbolTable(&tuple_vars,&symbolics,&exists,num_ufcalls);

  return reduced_symtable;
}

set<SRConjunction> SparseConstraints::convertToReduced(
                                         SymbolTable* orig_symtable,
                                         SymbolTable* reduced_symtable,
                                         map<string,string>& orig2reduced,
                                         set<SRConjunction> conjs) const{
  set<SRConjunction> new_conjs;

  //Convert all conjunctions
  for(set<SRConjunction>::const_iterator conj = conjs.begin();
      conj!=conjs.end(); ++conj) {
      list<TupleType> conj_tups=renameTupleVars(conj->tuplevarsBegin(),
          conj->tuplevarsEnd(),orig2reduced);
      MergeSymbolTableVisitor mstv(orig_symtable,reduced_symtable,
          &orig2reduced,conj_tups);
      conj->apply(&mstv);
      new_conjs.insert(mstv.getNewConjunction());
  }

  return new_conjs;
}

SRConjunction SparseConstraints::affineSimplify(SRConjunction conj,
                             SymbolTable *sym_table) const{
  //Separate affine and UFS constraints
  SRConjunction affine_conj=conj.getAffineConjunction();
  SRConjunction ufs_conj=conj.getUFSConjunction();

  //Create a new formula with just the affine constraints and get the string
  // of the affine formula
  string affine_formula_string;
  set<SRConjunction> affine_conjs;
  affine_conjs.insert(affine_conj);
  if(this->isSet){
    Set affine_set(new SymbolTable(*sym_table),affine_conjs,
                   this->inArity,this->context);
    affine_formula_string=affine_set.get_isl();
  }
  else{
    Relation affine_relation(new SymbolTable(*sym_table),affine_conjs,
                        this->inArity,this->outArity,this->context);
    affine_formula_string=affine_relation.get_isl();
  }

  //Ask ISL to simplify the new formula
  affine_formula_string=this->islSimplify(affine_formula_string);

  //Create a new simplified formula from the simplified string
  IEGenLibContext context(this->context);
  context.setSimplifyConjunctions(false);
  SymbolTable *affine_symtable;
  if(this->isSet){
    Set affine_set(affine_formula_string,context);
    affine_conj=*(affine_set.conSetBegin());
    affine_symtable=new SymbolTable(*affine_set.SymTable);
  }
  else{
    Relation affine_relation(affine_formula_string,context);
    affine_conj=*(affine_relation.conSetBegin());
    affine_symtable=new SymbolTable(*affine_relation.SymTable);
  }

  //Create a mapping from the affine formula's tuple names to the existing
  // set of tuple names in the given symbol table
  //TODO: Need to assert that we aren't mapping from a constant to a named
  //      tuple variable if ISL discovered that a dimension is constant
  map<string,string> affine2orig;
  list<TupleType>::const_iterator affine_tup,orig_tup;
  for(affine_tup=affine_conj.tuplevarsBegin(),
      orig_tup=ufs_conj.tuplevarsBegin();
      affine_tup!=affine_conj.tuplevarsEnd() &&
      orig_tup!=ufs_conj.tuplevarsEnd();
      ++affine_tup,++orig_tup){
    affine2orig[affine_tup->getName()]=orig_tup->getName();
  }

  //Convert the affine conjunction to the given symbol table
  list<TupleType> conj_tups=renameTupleVars(affine_conj.tuplevarsBegin(),
      affine_conj.tuplevarsEnd(),affine2orig);
  MergeSymbolTableVisitor mstv(affine_symtable,sym_table,&affine2orig,
                               conj_tups);
  affine_conj.apply(&mstv);
  affine_conj=mstv.getNewConjunction();
  delete affine_symtable;

  //Combine the simplified formula with the UFS constraints
  set<SREquality> final_eqs(affine_conj.equalitiesBegin(),
                            affine_conj.equalitiesEnd());
  for(set<SREquality>::const_iterator ufs_eq=ufs_conj.equalitiesBegin();
      ufs_eq!=ufs_conj.equalitiesEnd(); ++ufs_eq){
    final_eqs.insert(*ufs_eq);
  }
  set<SRInequality> final_ineqs(affine_conj.inequalitiesBegin(),
                                affine_conj.inequalitiesEnd());
  for(set<SRInequality>::const_iterator ufs_ineq=ufs_conj.inequalitiesBegin();
      ufs_ineq!=ufs_conj.inequalitiesEnd(); ++ufs_ineq){
    final_ineqs.insert(*ufs_ineq);
  }

  return SRConjunction(final_eqs,final_ineqs,
                       list<TupleType>(conj.tuplevarsBegin(),
                                       conj.tuplevarsEnd()));
}

string SparseConstraints::islSimplify(string affine_formula_string) const{
  //Input the affine formulla set/relation to the ISL code
  //The ISL code will remove the existential variables
  //and return the output set/relation in the ISL format
  isl_ctx *ctx=NULL;
  ctx=isl_ctx_alloc();
  isl_printer *printer=NULL;
  printer=isl_printer_to_str(ctx );
  //if the input string is Set
  if(this->isSet){
     isl_basic_set *set1;
     set1 =  isl_basic_set_read_from_str (ctx, affine_formula_string.c_str() , -1);
     isl_printer_set_output_format(printer , ISL_FORMAT_ISL);
     isl_printer_print_basic_set(printer ,set1);
     char *isl_set_str=isl_printer_get_str(printer);
     affine_formula_string = isl_set_str;
     isl_printer_flush(printer);
     free(isl_set_str);
     isl_basic_set_free(set1);
     set1= NULL;
  }
  //if the input string is Relation
  else{
     isl_basic_map *map1;
     map1 =  isl_basic_map_read_from_str (ctx, affine_formula_string.c_str() , -1);
     isl_printer_print_basic_map(printer ,map1);
     char *isl_map_str=isl_printer_get_str(printer);
     affine_formula_string = isl_map_str;
     isl_printer_flush(printer);
     free(isl_map_str);
     isl_basic_map_free(map1);
     map1= NULL;
   }
  //isl_printer_flush(printer);
  isl_printer_free(printer);
  printer=NULL;
  isl_ctx_free(ctx);
  ctx=NULL;
  //Replace the ": }" colon without constraints generated by the ISL format with "}" 
  string original = affine_formula_string.substr(affine_formula_string.size()-5, 4);
  if(original == ":  }"){
  affine_formula_string = affine_formula_string.substr(0, affine_formula_string.size()-5)+" }";
  }

  return affine_formula_string;
}

set<SRConjunction> SparseConstraints::getNewConjunctions(
                                        SymbolTable* merged_symbol_table,
                                        Relation const& other,
                                        map<string,string> old2newThis,
                                        map<string,string> old2newOther,
                                        int this_start, int this_end,
                                        int other_start, int other_end,
                                        int other_match_in, int other_match_out,
                                        list<TupleType> exists_eq_this,
                                        list<TupleType> exists_eq_other) const {
  set<SRConjunction> new_conjs;
  //Iterate over all pairs of conjunctions of this and other
  bool leg_conj;
  //sets that we dont have a 1=0 conjuction and a legal conjunction to false
  leg_conj = false;

  for(set<SRConjunction>::const_iterator itr_this = this->conSetBegin();
      itr_this!=this->conSetEnd(); ++itr_this) {
    for(set<SRConjunction>::const_iterator itr_other = other.conSetBegin();
        itr_other!=other.conSetEnd(); ++itr_other) {

      bool matching_constants;
      matching_constants = itr_this->check_for_matching_constants(*itr_other,
        other_match_in, other_match_out);


      if(matching_constants){
        //the new sets/list for the combined conjunction
        set<SREquality> combEq;
        set<SRInequality> combIeq;
        list<TupleType> combTup;

        //Create a new merged conjunction for this

        SRConjunction conjunction_this=*itr_this;
        list<TupleType> conj_tups_this=renameTupleVars(
            conjunction_this.tuplevarsBegin(),
            conjunction_this.tuplevarsEnd(),old2newThis);
        MergeSymbolTableVisitor mstv_this(this->SymTable,merged_symbol_table,
            &old2newThis,conj_tups_this);
        conjunction_this.apply(&mstv_this);
        conjunction_this=mstv_this.getNewConjunction();

        //Create a new merged conjunction for other
        SRConjunction conjunction_other=*itr_other;
        list<TupleType> conj_tups_other=renameTupleVars(
            conjunction_other.tuplevarsBegin(),
            conjunction_other.tuplevarsEnd(),old2newOther);
        MergeSymbolTableVisitor mstv_other(other.SymTable,merged_symbol_table,
            &old2newOther,conj_tups_other);
        conjunction_other.apply(&mstv_other);
        conjunction_other=mstv_other.getNewConjunction();


        //Create a combined conjunction from this and other
        //conjunction_this=conjunction_this+conjunction_other;
        combEq.insert(conjunction_this.equalitiesBegin(), conjunction_this.equalitiesEnd());
        combEq.insert(conjunction_other.equalitiesBegin(), conjunction_other.equalitiesEnd());

        combIeq.insert(conjunction_this.inequalitiesBegin(), conjunction_this.inequalitiesEnd());
        combIeq.insert(conjunction_other.inequalitiesBegin(), conjunction_other.inequalitiesEnd());

        //create the new tuple list
        combTup = itr_this->make_new_tuple_list(conj_tups_this,conj_tups_other,
            this_start, this_end, other_start, other_end);

        list<TupleType>::const_iterator it_other = exists_eq_other.begin();
        for(list<TupleType>::const_iterator it_this = exists_eq_this.begin();
            it_this != exists_eq_this.end(); ++it_this){
          if(it_other->isVar() && it_this->isVar()){
            ExpVec orig = merged_symbol_table->constructExpVec(old2newThis[it_this->getName()],1);
            ExpVec dup = merged_symbol_table->constructExpVec(old2newOther[it_other->getName()],-1);
            ExpVec sum = orig+dup;
            combEq.insert(SREquality(sum));
            ++it_other;
          }else if(it_other->isVar() && it_this->isConst()){
            ExpVec exv = merged_symbol_table->constructExpVec(old2newOther[it_other->getName()],1);
            exv.set_const(-1*it_this->getValue());
            combEq.insert(SREquality(exv));
            ++it_other;
          }else if(it_other->isConst() && it_this->isVar()){
            ExpVec exv = merged_symbol_table->constructExpVec(old2newThis[it_this->getName()],1);
            exv.set_const(-1*it_other->getValue());
            combEq.insert(SREquality(exv));
            ++it_other;
          }else if(it_other->isConst() && it_this->isConst()){
            ++it_other;
          }
        }

        SRConjunction combConj(combEq, combIeq, combTup);

        //Add the newly created conjunction
        new_conjs.insert(combConj);
        leg_conj = true; //we have at least one legal conjunction
      }else{//This is for a 1=0 conjunction done at the end if needed
      }
    }
  }

  if(!leg_conj){
    //we have no legal conjunctions so we must at 1=0
    set<SREquality> combEq;
    set<SRInequality> combIeq;
    list<TupleType> combTup;
    combEq.insert(SREquality(merged_symbol_table->constructExpVec(1)));
    list<TupleType> conj_tups_this=renameTupleVars(
        this->conSetBegin()->tuplevarsBegin(),this->conSetBegin()->tuplevarsEnd(),old2newThis);
    list<TupleType> conj_tups_other=renameTupleVars(
        other.conSetBegin()->tuplevarsBegin(),other.conSetBegin()->tuplevarsEnd(),old2newOther);
    combTup=this->conSetBegin()->make_new_tuple_list(conj_tups_this,conj_tups_other,
      this_start, this_end, other_start, other_end);
    SRConjunction combConj(combEq, combIeq, combTup);
    new_conjs.insert(combConj);
  }

  return new_conjs;
}
/******************************************************************************/

/********************************** Set ***************************************/
string Set::get_isl() const{
  SetRelationISLVisitor isl;
  this->apply(&isl);
  return isl.getISL();
}

string Set::get_dot(){
  SetRelationDotVisitor dot;
  this->apply(&dot);
  return dot.returnString();
}

string Set::getAST(){
  return astDot;
}

void Set::apply(SRVisitor* visitor) const{
  visitor->SetCase(this);
}

void Set::applySpCon(SRVisitor* visitor) const{
  visitor->SparseConstraintsCase(this);
}

bool Set::operator==(Set const& other) const{
  //STEP 1: Check for same arity between sets AND that no existential variables
  //        are present in either set
  //Ensure that the context is the same between the two sets
  if(this->context!=other.context) {
    throw OperatorEqualsException("Cannot use == on sets with different contexts.");
  }
  if(SymTable->containsExistVars() || other.SymTable->containsExistVars()) {
    throw OperatorEqualsException ("Cannot use == on sets with existential variables.");
  }
  return inArity == other.inArity && SparseConstraints::operator==(other);
}

Set Set::Union(Set const& other) const{
  //STEP 1: Check that arity of this matches arity of other, raise an exception
  //        if this is not the case
  //Ensure that the context is the same between the sets
  if(this->context.getSimplifyConjunctions()!=other.context.getSimplifyConjunctions()) {
    throw UnionException("Cannot use a union on sets with different contexts.");
  }
  /*if(this->context!=other.context) {
    throw UnionException("Cannot use a union on sets with different contexts.");
  }*/
  SparseConstraints::checkArity(other);
  SparseConstraints::checkConstVarMatchforUnion(other);

  //Union the contexts from both set and relation
  //Union the symbolics and InversePair names
  set<Symbolic> otherSymbolics = other.context.getSymbolics();
  set<pair<string,string> > otherInversePairs = other.context.getInversePairs();
  IEGenLibContext UnionContext(this->context);
  for(set<Symbolic>::iterator itr =otherSymbolics.begin() ; itr != otherSymbolics.end(); itr++){
     UnionContext.addSymbolic( *itr );
  }
  for(set<pair<string,string> >::iterator itr =otherInversePairs.begin() ; itr != otherInversePairs.end(); itr++){
      string name1 = (*itr).first;
      string name2 = (*itr).second;
      if(!UnionContext.hasInverse(name1,name2) ){
        UnionContext.addInversePair(name1, name2);
      }
  }

  pair<SymbolTable*,set<SRConjunction> > res=SparseConstraints::Union(other);
  return Set(res.first,res.second,this->getArity(),UnionContext); //this->context changed to UnionContext
  // the return ststement was: Set(res.first,res.second,this->getArity(),UnionContext).simplify();
}

Set Set::simplify() const{
  //Call the common simplify implementation in SparseConstraints
  pair<SymbolTable*,set<SRConjunction> > res=SparseConstraints::simplify();

  return Set(res.first,res.second,this->getArity(),this->context);
}
/******************************************************************************/

/******************************** Relation ************************************/
string Relation::get_isl() const{
  SetRelationISLVisitor isl;
  this->apply(&isl);
  return isl.getISL();
}

string Relation::get_dot(){
  SetRelationDotVisitor dot;
  this->apply(&dot);
  return dot.returnString();
}

string Relation::getAST(){
  return astDot;
}

void Relation::apply(SRVisitor* visitor) const{
  visitor->RelationCase(this);
}

void Relation::applySpCon(SRVisitor* visitor) const{
  visitor->SparseConstraintsCase(this);
}

Relation Relation::Inverse() const{
  set<string> tuple_vars, symbolics, existentials, symbols;
  list<string> tuple_vars_this, tuple_vars_other;
  list<TupleType> invertedTupleVars;
  map<string, string> old2new;
  SymbolTable *invertedST;

  symbolics = set<string>(this->SymTable->symNamesBegin(), this->SymTable->symNamesEnd());
  existentials = set<string>(this->SymTable->existNamesBegin(), this->SymTable->existNamesEnd());

  //Create the list of tuple variables for the new symbol table using this relation's tuple types
  //(note, may be unnecessary due to symbol table having the exact same variables, should be used for the map instead)


//  tuple_vars_this=this->getTupleVarNames();
//  tuple_vars_this=createUniqueNames(tuple_vars_this.begin(),
//    tuple_vars_this.end(),symbols,old2newThis);

  list<string> tmpTuples(this->getTupleVarNames());
  tuple_vars=set<string>(tmpTuples.begin(),tmpTuples.end());
 
  //Create the "inverted" new symbol table
  invertedST = new SymbolTable(&tuple_vars, &symbolics, &existentials,
                               this->SymTable->getNumFuncs());

  set<SRConjunction> new_conjs;

  for(set<SRConjunction>::const_iterator conItr = this->conSetBegin();
      conItr!=this->conSetEnd(); ++conItr){

    list<TupleType> invertedTupleVars1;
    SRConjunction conjunction=*conItr;

    vector<TupleType> currVars;
    for(list<TupleType>::const_iterator itr = conItr->tuplevarsBegin(); itr != conItr->tuplevarsEnd(); ++itr){
      currVars.push_back((*itr));
      if(itr->isVar()) old2new[itr->getName()] = itr->getName();
    }
    for(int i = inArity; i < inArity + outArity; i++){
      invertedTupleVars1.push_back(currVars.at(i));
    }
    for(int i = 0; i < inArity; i++){
      invertedTupleVars1.push_back(currVars.at(i));
    }
    SRConjunction tmp(set<SREquality>(conjunction.equalitiesBegin(), conjunction.equalitiesEnd()), set<SRInequality>(conjunction.inequalitiesBegin(), conjunction.inequalitiesEnd()), invertedTupleVars1);
    MergeSymbolTableVisitor mstv(this->SymTable,invertedST,
          &old2new,invertedTupleVars1);
    tmp.apply(&mstv);
    new_conjs.insert(mstv.getNewConjunction());
  }


  return Relation(invertedST,new_conjs,this->getOutArity(),
    this->getInArity(),this->context).simplify();
}

Set Relation::Apply(Set const& other) const{

  set<string> symbolics,exists,tuple_vars;
  list<string> symbolics_this,symbolics_other;
  list<string> exists_this,exists_other;
  list<TupleType> exists_eq_this,exists_eq_other;
  list<string> tuple_vars_this,tuple_vars_other;
  int num_ufcalls;
  set<string> symbols;
  map<string,string> old2newThis, old2newOther;
  SymbolTable *merged_symbol_table;

  int this_start = this->inArity; 
  int this_end = this->outArity - 1 + this_start;
  int other_start = -1;//gives the starting location for the out tuple
  int other_end = -1; //gives the end of out tuple
  int this_match_out = this->inArity - 1;
  int this_match_in = 0;

  //STEP 1: Check that in arity of other matches out arity of this, raise an
  //        exception if this is not the case
  //      respect to named vs. constant TupleTypes.  This will require a routine
  //      similar to checkConstVarMatchforUnion but will take a range for each
  //      relation to check
  //Ensure that the context is the same between the set and relation
  if(this->context.getSimplifyConjunctions()!=other.context.getSimplifyConjunctions()) {
    throw ApplyException("Cannot use on a set and relation with different contexts.");
  }

  if(other.inArity != this->getInArity()){
    throw ApplyException("The Arity does not match");
  }

  //STEP 2: Gather info for new symbol table
  //Gather symbolics from both formulas
  symbolics_this=createUniqueNames(this->SymTable->symNamesBegin(),
    this->SymTable->symNamesEnd(),symbols,old2newThis);
  symbolics_other=createUniqueNames(other.SymTable->symNamesBegin(),
    other.SymTable->symNamesEnd(),symbols,old2newOther);
  symbolics=unionNamesLists(symbolics_other, symbolics_this);

  //Union the contexts from both set and relation
  //Union the symbolics and InversePair names
  set<Symbolic> otherSymbolics = other.context.getSymbolics();
  set<pair<string,string> > otherInversePairs = other.context.getInversePairs();
  IEGenLibContext UnionContext(this->context);
  for(set<Symbolic>::iterator itr =otherSymbolics.begin() ; itr != otherSymbolics.end(); itr++){
     UnionContext.addSymbolic( *itr );
  }
  for(set<pair<string,string> >::iterator itr =otherInversePairs.begin() ; itr != otherInversePairs.end(); itr++){
      string name1 = (*itr).first;
      string name2 = (*itr).second;
      if(!UnionContext.hasInverse(name1,name2) ){
        UnionContext.addInversePair(name1, name2);
      }
  }

  //Gather tuple variables from both formulas
  tuple_vars_other=this->getOutputTupleVarNames();
  tuple_vars_other=createUniqueNames(tuple_vars_other.begin(),
    tuple_vars_other.end(),symbols,old2newThis);
  tuple_vars.insert(tuple_vars_other.begin(),tuple_vars_other.end());

  //Gather existential variables from both formulas
  exists_this=this->getInputTupleVarNames();
  exists_this=createUniqueNames(exists_this.begin(),exists_this.end(),
                                 symbols,old2newThis);
  exists_other=other.getInputTupleVarNames();
  exists_other=createUniqueNames(exists_other.begin(),exists_other.end(),
                                 symbols,old2newOther);
  exists=unionNamesLists(exists_other, exists_this);
  exists_eq_this = this->getInputTupleVarTypes();
  exists_eq_other = other.getInputTupleVarTypes();

  exists_this=createUniqueNames(this->SymTable->existNamesBegin(),
    this->SymTable->existNamesEnd(),symbols,old2newThis);
  exists_other=createUniqueNames(other.SymTable->existNamesBegin(),
    other.SymTable->existNamesEnd(),symbols,old2newOther);
  exists.insert(exists_other.begin(),exists_other.end());
  exists.insert(exists_this.begin(),exists_this.end());


  //Calculate the upper bound on the number of function calls
  num_ufcalls = this->SymTable->getNumFuncs() + other.SymTable->getNumFuncs();

  //STEP 3: Create a symbol table based on the information gathered above
  merged_symbol_table=new SymbolTable(&tuple_vars,&symbolics,&exists,
    num_ufcalls);

  //STEP 4: Create new set of conjunctions
  set<SRConjunction> new_conjs = other.getNewConjunctions(merged_symbol_table, *this, old2newOther, old2newThis, other_start, other_end, this_start, this_end, this_match_in, this_match_out, exists_eq_other, exists_eq_this);

  return Set(merged_symbol_table,new_conjs,this->getOutArity(), UnionContext).simplify(); //this->context changed to UnionContext
}

bool Relation::operator==(Relation const& other) const{
  //STEP 1: Check for any existential variables in both Relations
  //Ensure that the context is the same between the two relations
  if(this->context!=other.context) {
    throw OperatorEqualsException("Cannot use == on relations with different contexts.");
  }
  if(SymTable->containsExistVars() || other.SymTable->containsExistVars()) {
    throw OperatorEqualsException("Cannot use == on relations with existential variables.");
  }

  //STEP 2: Check for same in and out arity between both relations
  return inArity == other.inArity && outArity == other.outArity && SparseConstraints::operator==(other);
}

Relation Relation::Union(Relation const& other) const{
  //STEP 1: Check that arity of this matches arity of other, raise an exception
  //        if this is not the case
  //Ensure that the context is the same between the relations
  if(this->context.getSimplifyConjunctions()!=other.context.getSimplifyConjunctions()) {
    throw UnionException("Cannot use a union on relations with different contexts.");
  }
  /*if(this->context!=other.context) {
    throw UnionException("Cannot use a union on relations with different contexts.");
  }*/
  SparseConstraints::checkArity(other);
  SparseConstraints::checkConstVarMatchforUnion(other);

  //Union the contexts from both set and relation
  //Union the symbolics and InversePair names
  set<Symbolic> otherSymbolics = other.context.getSymbolics();
  set<pair<string,string> > otherInversePairs = other.context.getInversePairs();
  IEGenLibContext UnionContext(this->context);
  for(set<Symbolic>::iterator itr =otherSymbolics.begin() ; itr != otherSymbolics.end(); itr++){
     UnionContext.addSymbolic( *itr );
  }
  for(set<pair<string,string> >::iterator itr =otherInversePairs.begin() ; itr != otherInversePairs.end(); itr++){
      string name1 = (*itr).first;
      string name2 = (*itr).second;
      if(!UnionContext.hasInverse(name1,name2) ){
        UnionContext.addInversePair(name1, name2);
      }
  }

  //Call the common union implementation in SparseConstraints
  pair<SymbolTable*,set<SRConjunction> > res=SparseConstraints::Union(other);

  return Relation(res.first,res.second,this->getInArity(),this->getOutArity(),UnionContext); 
  //this->context changed to UnionContext
  // the return ststement was: Relation(res.first,res.second,this->getArity(),UnionContext).simplify();
}

Relation Relation::Compose(Relation const & other) const{
  set<string> symbolics,exists,tuple_vars;
  list<string> symbolics_this,symbolics_other;
  list<string> exists_this,exists_other;
  list<TupleType> exists_eq_this,exists_eq_other;
  list<string> tuple_vars_this,tuple_vars_other;
  int num_ufcalls;
  set<string> symbols;
  map<string,string> old2newThis, old2newOther;
  SymbolTable *merged_symbol_table;
  int this_start = this->inArity;//gives the starting location for the out tuple
  int this_end = this->outArity - 1 + this_start; //gives the end of the out tuple
  int other_start = 0;
  int other_end = other.inArity - 1;
  int other_match_out = other.inArity + other.outArity - 1;
  int other_match_in = other.inArity;

  //STEP 1: Check that in arity of this matches out arity of other, raise an
  //        exception if this is not the case
  //      respect to named vs. constant TupleTypes.  This will require a routine
  //      similar to checkConstVarMatchforUnion but will take a range for each
  //      relation to check
  //Ensure that the context is the same between the relations
  if(this->context.getSimplifyConjunctions()!=other.context.getSimplifyConjunctions()) {
    throw ComposeException("Cannot use a compose on relations with different contexts.");
  }
  /*if(this->context!=other.context) {
    throw ComposeException("Cannot use a compose on relations with different contexts.");
  }*/
  if(this->inArity != other.outArity){
    throw ComposeException("The Arity does not match");
  }

  //STEP 2: Gather info for new symbol table
  //Gather symbolics from both formulas
  symbolics_this=createUniqueNames(this->SymTable->symNamesBegin(),
    this->SymTable->symNamesEnd(),symbols,old2newThis);
  symbolics_other=createUniqueNames(other.SymTable->symNamesBegin(),
    other.SymTable->symNamesEnd(),symbols,old2newOther);
  symbolics=unionNamesLists(symbolics_this,symbolics_other);

  //Union the contexts from both set and relation
  //Union the symbolics and InversePair names
  set<Symbolic> otherSymbolics = other.context.getSymbolics();
  set<pair<string,string> > otherInversePairs = other.context.getInversePairs();
  IEGenLibContext UnionContext(this->context);
  for(set<Symbolic>::iterator itr =otherSymbolics.begin() ; itr != otherSymbolics.end(); itr++){
     UnionContext.addSymbolic( *itr );
  }
  for(set<pair<string,string> >::iterator itr =otherInversePairs.begin() ; itr != otherInversePairs.end(); itr++){
      string name1 = (*itr).first;
      string name2 = (*itr).second;
      if(!UnionContext.hasInverse(name1,name2) ){
        UnionContext.addInversePair(name1, name2);
      }
  }

  //Gather tuple variables from both formulas
  tuple_vars_other=other.getInputTupleVarNames();
  tuple_vars_other=createUniqueNames(tuple_vars_other.begin(),
    tuple_vars_other.end(),symbols,old2newOther);
  tuple_vars_this=this->getOutputTupleVarNames();
  tuple_vars_this=createUniqueNames(tuple_vars_this.begin(),
    tuple_vars_this.end(),symbols,old2newThis);

  tuple_vars.insert(tuple_vars_other.begin(),tuple_vars_other.end());
  tuple_vars.insert(tuple_vars_this.begin(),tuple_vars_this.end());
  //Gather existential variables from both formulas
  exists_other=other.getOutputTupleVarNames();
  exists_other=createUniqueNames(exists_other.begin(),exists_other.end(),
                                 symbols,old2newOther);
  exists_this=this->getInputTupleVarNames();
  exists_this=createUniqueNames(exists_this.begin(),exists_this.end(),
                                 symbols,old2newThis);
  exists=unionNamesLists(exists_this,exists_other);
  //these will be the new exists from this and other this is used in the for loop
  //in step 4 to create the equal expvecs
  exists_eq_this = this->getInputTupleVarTypes();
  exists_eq_other = other.getOutputTupleVarTypes();

  exists_this=createUniqueNames(this->SymTable->existNamesBegin(),
    this->SymTable->existNamesEnd(),symbols,old2newThis);
  exists_other=createUniqueNames(other.SymTable->existNamesBegin(),
    other.SymTable->existNamesEnd(),symbols,old2newOther);
  exists.insert(exists_this.begin(),exists_this.end());
  exists.insert(exists_other.begin(),exists_other.end());

  //Calculate the upper bound on the number of function calls
  num_ufcalls = this->SymTable->getNumFuncs() + other.SymTable->getNumFuncs();

  //STEP 3: Create a symbol table based on the information gathered above
  merged_symbol_table=new SymbolTable(&tuple_vars,&symbolics,&exists,
    num_ufcalls);

  //STEP 4: Create new set of conjunctions
  set<SRConjunction> new_conjs = this->getNewConjunctions(merged_symbol_table, other, old2newThis, old2newOther, this_start, this_end, other_start, other_end, other_match_in, other_match_out, exists_eq_this, exists_eq_other);

  return Relation(merged_symbol_table,new_conjs,other.getInArity(),
    this->getOutArity(),UnionContext).simplify(); //this->context changed to UnionContext
}

Relation Relation::simplify() const{
  //Call the common union implementation in SparseConstraints
  pair<SymbolTable*,set<SRConjunction> > res=SparseConstraints::simplify();

  return Relation(res.first,res.second,this->getInArity(),this->getOutArity(),this->context);
}
/******************************************************************************/

}//end namespace iegenlib
